***
*** the MCS mutual exclusion protocol
***

*** Variables:
***   glock : Pid, initially nop, shared with all processes
***   next_p : Pid, initially nop
***   lock_p : Bool, initially false
***   pred_p : Pid, initially nop
*** 
*** A pseudo-code of the MCS protocol for each process p:
*** 
*** ss:  \"Remainder Section\"
*** l1:  next_p := nop;
*** l2:  pred_p := fetch&store(glock,p);
*** l3:  if pred_p =/= nop {
*** l4:    lock_p := true;
*** l5:    next_{pred_p} := p;
*** ws:    repeat while lock_p; }
*** cs:  \"Critical Section\"
*** l7:  if next_p = nop {
*** l8:    if comp&swap(glock,p,nop)
*** l9:      goto fs;
*** l10:   repeat while next_p = nop; }
*** l11: locked_{next_p} := false;
*** fs:  \"Finish Section\"
*** 
*** where
*** 
*** fetch&store(x,v) does the following atomically:
*** tmp := x, x := v, and tmp is returned.
*** 
*** comp&swap(x,v1,v2) does the following atomically:
*** if x = v1, then x := v2 and true is returned,
*** Otherwise, false is returned.
***

fmod LABEL is
  sort Label .
  ops l1 l2 l3 l4 l5 ws l7 l8 l9 l10 l11 fs ss cs : -> Label [ctor] .
endfm

fmod PID is
  sort Pid .
  --- nop is a dummy process ID.
  ops p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 nop : -> Pid [ctor] .
endfm

fmod SOUP {D :: TRIV} is
  sort Soup{D} .
  subsort D$Elt < Soup{D} .
  op empty : -> Soup{D} [ctor] .
  op _ _ : Soup{D} Soup{D} -> Soup{D} [ctor assoc comm id: empty] .
endfm

fmod NAT+DEC is
  pr NAT .
  op dec : Nat -> Nat .
  var N : Nat .
  eq dec(0) = 0 .
  eq dec(s(N)) = N .
endfm

fmod OCOMP is
  pr LABEL .
  pr PID .
  pr NAT+DEC .
  sort OComp .
  --- observable components
  op glock:_ : Pid -> OComp [ctor] .
  op (pc[_]:_) : Pid Label -> OComp [ctor] .
  op (next[_]:_) : Pid Pid -> OComp [ctor] .
  op (lock[_]:_) : Pid Bool -> OComp [ctor] .
  op (pred[_]:_) : Pid Pid -> OComp [ctor] .
  op (cnt:_) :  Nat -> OComp [ctor] .
endfm
  
view OComp from TRIV to OCOMP is
  sort Elt to OComp .
endv

fmod CONFIG is
  pr SOUP{OComp} .
  sort Config .
  op {_} : Soup{OComp} -> Config [ctor] .
  op init3 : -> Config .
  op init5 : -> Config .
  op init6 : -> Config .
  eq init3
  = {(glock: nop)
       (pc[p1]: ss) (pc[p2]: ss) (pc[p3]: ss) 
       (next[p1]: nop) (next[p2]: nop)  (next[p3]: nop)
       (lock[p1]: false) (lock[p2]: false)  (lock[p3]: false)
       (pred[p1]: nop) (pred[p2]: nop) (pred[p3]: nop) (cnt: 3)} .
  eq init5
  = {(glock: nop)
       (pc[p1]: ss) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) 
       (next[p1]: nop) (next[p2]: nop)  (next[p3]: nop) (next[p4]: nop) (next[p5]: nop)
       (lock[p1]: false) (lock[p2]: false)  (lock[p3]: false)  (lock[p4]: false)  (lock[p5]: false)
       (pred[p1]: nop) (pred[p2]: nop) (pred[p3]: nop) (pred[p4]: nop) (pred[p5]: nop) (cnt: 5)} .
  eq init6
  = {(glock: nop)
       (pc[p1]: ss) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) 
       (next[p1]: nop) (next[p2]: nop)  (next[p3]: nop) (next[p4]: nop) (next[p5]: nop) (next[p6]: nop)
       (lock[p1]: false) (lock[p2]: false)  (lock[p3]: false)  (lock[p4]: false) (lock[p5]: false) (lock[p6]: false)
       (pred[p1]: nop) (pred[p2]: nop) (pred[p3]: nop) (pred[p4]: nop) (pred[p5]: nop)  (pred[p6]: nop) 
       (cnt: 6)} .
endfm

mod MCS is
  pr CONFIG .
  --- Maude vars
  vars P Q Q1 : Pid .
  var L : Label .
  var B : Bool .
  var N : Nat .
  var OCs : Soup{OComp} .
  --- want 
  rl [want] : {(pc[P]: ss) OCs} => {(pc[P]: l1) OCs} .
  --- stnxt  
  rl [stnxt] : {(pc[P]: l1) (next[P]: Q) OCs} => {(pc[P]: l2) (next[P]: nop) OCs} .
  --- stprd  
  rl [stprd] :  {(glock: Q) (pc[P]: l2) (pred[P]: Q1) OCs}
  => {(glock: P) (pc[P]: l3) (pred[P]: Q) OCs} .
  --- chprd  
  rl [chprd] :  {(pc[P]: l3) (pred[P]: Q) OCs}
  => {(pc[P]: (if Q == nop then cs else l4 fi)) (pred[P]: Q) OCs} .
  --- stlck  
  rl [stlck] : {(pc[P]: l4) (lock[P]: B) OCs} => {(pc[P]: l5) (lock[P]: true) OCs} .
  --- stnpr  
  rl [stnpr] : {(pc[P]: l5) (pred[P]: Q) (next[Q]: Q1) OCs}
  => {(pc[P]: ws) (pred[P]: Q) (next[Q]: P) OCs} .
  --- chlck  
  rl [chlck] : {(pc[P]: ws) (lock[P]: false) OCs}
  => {(pc[P]: cs) (lock[P]: false) OCs} .
***(
  rl [chlck] : {(pc[P]: ws) (lock[P]: B) OCs}
  => {(pc[P]: (if B then ws else cs fi)) (lock[P]: B) OCs} .
)***
  --- exit  
  rl [exit] : {(pc[P]: cs) OCs} => {(pc[P]: l7) OCs} .
  --- rpnxt  
  rl [rpnxt] : {(pc[P]: l7) (next[P]: Q) OCs}
  => {(pc[P]: (if Q == nop then l8 else l11 fi)) (next[P]: Q) OCs} .
  --- chglk  
  rl [chglk] : {(glock: Q) (pc[P]: l8) OCs}
  => {(glock: (if Q == P then nop else Q fi)) (pc[P]: (if Q == P then l9 else l10 fi)) OCs} .
  --- go2rs  
  rl [go2rs] : {(pc[P]: l9) (cnt: N) OCs} => {(pc[P]: fs) (cnt: dec(N)) OCs} .
  --- rpnxt  
  crl [rpnxt] : {(pc[P]: l10) (next[P]: Q) OCs}
  => {(pc[P]: l11) (next[P]: Q) OCs}
  if Q =/= nop .
  --- stlnx  
  rl [stlnx] : {(pc[P]: l11) (next[P]: Q) (lock[Q]: B) (cnt: N) OCs}
  => {(pc[P]: fs) (next[P]: Q) (lock[Q]: false) (cnt: dec(N)) OCs} .
  --- fin
  rl [fin] : {(cnt: 0) OCs} => {(cnt: 0) OCs} .
endm

in model-checker .

mod MCS-PREDS is
  pr MCS .
  inc SATISFACTION .
  subsort Config < State .
  op inWs1 : -> Prop .
  op inCs1 : -> Prop .
  var PROP : Prop .
  var OCs :  Soup{OComp} .
  eq {(pc[p1] : ws) OCs} |= inWs1 = true .
  eq {(pc[p1] : cs) OCs} |= inCs1 = true .
  eq {OCs} |= PROP = false [owise] .
endm

mod MCS-CHECK is
  inc MCS-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
  op lofree1 : -> Formula .
  eq lofree1 = inWs1 |-> inCs1 .
endm